D:Dsys, v:(i:IdM(i).state), sched:(Id((IdLnk+Id)+Unit)),
dec:(i,a:IdM(i).state(M(i).da(locl(a))+Unit)).
Feasible(D)  d-world(D;v;sched;dec)  World 

latex

Definitions

Top, IdLnk, x:A. B(x), source(l), M(i), M.dout(l,tg), x.A(x), locl(a), M.da(a), M.ds(x), w-automaton(T;TA;M), x:AB(x), mlnk(m), Msg(M), {x:A| B(x) }, type List, w-action-dec(TA;M;i), Action(dec), <a,b>, f(a), P  Q, False, A, AB, , 1of(t), f(x)?z, CV(F), M.init(x)?v, i=j, if b t else f fi, d-world(D;v;sched;dec), World, Dsys, M.state, Unit, left+right, Feasible(D), Type, Void, t  T, d-comp(D;v;sched;dec), d-world-state(D;i), Id, x:AB(x), #$n, {i..j}, , s = t, Prop, b, b, , P & Q, P  Q, State(ds), n-m, -n, n+m, a<b, Knd, 2of(t), rcv(l,tg), S  T, Msg(da), M.Msg, x:A. B(x), , d-machine(i;M;dec)

Lemmas

d-machine wf, it wf, subtype rel list, ma-msg wf, mlnk wf d, CV wf, le wf, subtype rel self, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, bool wf, bnot wf, not wf, assert wf, d-feasible wf, unit wf, ma-st wf, dsys wf, d-comp wf2, int seg wf, d-world-state wf, ifthenelse wf, eq int wf, ma-init-val wf, action wf, w-action-dec wf, nat wf, Msg wf, mlnk wf, w-automaton wf, ma-ds wf, ma-da wf, locl wf, ma-dout wf, d-m wf, lsrc wf, Id wf, IdLnk wf, top wf